﻿// Jinx AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Formality.FormalSystem.Parser;

namespace Formality.FormalSystem.Reasoning.Rewrite
{
    public class Search : IJustificationSearch
    {
        public Search(Proposition PossibleDefinition, Proposition Goal, Proposition[] Premises)
        {
            if (PossibleDefinition.IsDefinition)
                Definition = new Definition(PossibleDefinition);

            this.Goal = Goal;
            this.Premises = Premises;
        }

        #region IJustificationSearch Members

        Reasoning.Justification IJustificationSearch.Perform()
        {
            if (Definition == null)
                return null;

            // Try the definition both ways
            return Try(Definition.Definiendum, Definition.Definiens, Goal, Premises)
                   ?? Try(Definition.Definiens, Definition.Definiendum, Goal, Premises);
        }

        #endregion

        private Definition Definition;
        private Proposition Goal;
        private Proposition[] Premises;

        // Search for a premise which can be rewritten into our goal
        private static Justification Try(Proposition Definiendum, Proposition Definiens, Proposition Goal, Proposition[] Premises)
        {
            if (Premises.Any(p => Try(Definiendum, Definiens, Goal, p)))
                return new Justification();

            return null;
        }

        private static bool Try(Proposition Definiendum, Proposition Definiens, Proposition Goal, Proposition Premise)
        {
            if (Premise == Goal)
                return true;

            if (CheckApplication(Definiendum, Definiens, Premise, Goal))
                return true;

            if (Premise.Operator != Goal.Operator)
                return false;

            if (Premise.Variables != Goal.Variables)
                return false;

            if (Premise.Operands.Length != Goal.Operands.Length)
                return false;

            for (var i = 0; i < Goal.Operands.Length; i++)
            {
                if (Premise.Operands[i] != Goal.Operands[i])
                    if (!Try(Definiendum, Definiens, Goal.Operands[i], Premise.Operands[i]))
                        return false;
            }

            return true;
        }

        public static bool CheckApplication(Proposition Definiendum, Proposition Definiens, Proposition Premise, Proposition Goal)
        {
            Premise = Premise.Bind();
            Goal = Goal.Bind();

            var Application = Apply(Definiendum, Definiens, Premise);

            if (Application == null)
                return false;

            if (Application == Goal)
                return true;

            var VarRename = new VariableRenaming.Search(Application, Goal).Perform();

            if (VarRename == null)
                return false;

            return VarRename.Map.All(m => m.Key == m.Value);
        }

        public static Proposition Apply(Proposition Definiendum, Proposition Definiens, Proposition Premise)
        {
            var Attempt = new FunctionSubstitution.Search(Definiendum, Premise);

            var Sub = Attempt.Perform();

            if (Sub == null) return null;

            return Sub.SubstitutionMap.ApplySubstitutions(Definiens);
        }

        private static bool Issub(Proposition p, Proposition Potential)
        {
            var Attempt = new FunctionSubstitution.Search(Potential, p, false);

            return (Attempt.Perform() != null);
        }

        public static IEnumerable<Proposition> ApplyTemplate(Proposition Definiendum, Proposition Definiens, Proposition Goal)
        {
            return ApplyTemplate(Definiendum, Definiens, Goal, new Bindings());
        }

        public static IEnumerable<Proposition> ApplyTemplate(Proposition Definiendum, Proposition Definiens, Proposition Goal, Bindings Bindings)
        {
            var Attempt = new FunctionSubstitution.Search(Definiendum, Goal, false);
            var Justification = Attempt.Perform();

            if (Justification != null)
                yield return Justification.SubstitutionMap.ApplySubstitutions(Definiens).Bind(Bindings);

            if (Goal.Type == PropType.Binder) foreach (var v in Goal.Variables) Bindings.Bind(v);

            var Ops = Goal.Operands;
            for (var i = 0; i < Ops.Length; i++)
            {
                var Op = Ops[i];

                foreach (var ReplacementOp in ApplyTemplate(Definiendum, Definiens, Op, Bindings))
                {
                    var RepArray = new Proposition[Ops.Length];

                    for (var j = 0; j < Ops.Length; j++)
                        RepArray[j] = (j == i) ? ReplacementOp : Ops[j];

                    yield return new Proposition(Goal, v => v, RepArray);
                }
            }

            if (Goal.Type == PropType.Binder) foreach (var v in Goal.Variables) Bindings.Unbind(v);
        }
    }
}
